\begin{tabbing}
$\forall$\=${\it es}$:ES, $T$, $A$:Type, $l$:IdLnk, ${\it tg}$, $a$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $P$:(State(${\it ds}$)$\rightarrow$$A$$\rightarrow$Prop),\+
\\[0ex]$f$:(State(${\it ds}$)$\rightarrow$$A$$\rightarrow$$T$).
\-\\[0ex]weak{-}precond{-}send{-}p(${\it es}$;$T$;$A$;$l$;${\it tg}$;$a$;${\it ds}$;$P$;$f$) $\in$ Prop
\end{tabbing}